COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	provin[f81,jmc]		Notes for revising chapter 3 of McCarthy and Talcott
C00003 00003	Replacing programs by sentences
C00014 00004	new outline
C00016 00005	logic for the Cobol programmer
C00025 00006	Expressions used in recursive programs
C00030 00007	Notes on the old chapter
C00032 00008	Proof techniques
C00034 ENDMK
C⊗;
provin[f81,jmc]		Notes for revising chapter 3 of McCarthy and Talcott

Very often we have to prove that an argument is of the right sort in
order to substitute into a function definition.  Some more explicit
recognition of this is needed.  The EKL sortlist may even be appropriate.
Replacing programs by sentences

	Proving assertions about pure LISP programs is based on
the fact that a recursive program may be converted
into a sentence of
mathematical logic by replacing
the ← sign by an = sign and adding quantifiers to assert that the
sentence is true for all values of the variables in the appropriate
domain.  Because of certain mathematical theorems not proved in this text,
this sentence in combination with axioms about
the basic functions of LISP can be used to prove sentences involving the function
symbol of the program that in turn express extensional facts
about the program.

	An easy example is the program for ⊗append 

⊗⊗⊗u * v ← qif qn u qthen v qelse qa u . [qd u * v]⊗

which is converted into the sentence

⊗⊗⊗∀u v.(u * v = qif qn u qthen v qelse qa u . [qd u * v])⊗,

which in turn can be used to write sentences like

⊗⊗⊗∀u v w.[(u * v) * w = u * (v * w)]⊗,

which expresses the fact that the ⊗append operation is associative.
We will show how to prove this and other such sentences.

	Replacing the program by the sentence depends on a mathematical
theorem asserting that the function computed by the LISP program satisfies
the sentence.  This is always true provided we interpret the sentence
in a suitable way.  Our immediate goal is to express this correspondence
precisely as a mathematical theorem.

	We begin with the computation performed by the program.
Actual LISP systems involve compilers and interpreters which are complicated
to describe and differ among implementations.  These compilers and
interpreters do much
more than execute pure LISP programs.  Therefore, we shall describe the
computation performed by the program by another rule.  Indeed we
regard this description as the definition of pure LISP and regard
a compiler or interpreter as correct for pure LISP only if its computation
corresponds to this computation rule.

	Consider a pure LISP program 

⊗⊗⊗f(x,y) ← qt(x,y,f)⊗,

the right hand side of which may involve elementary LISP functions,
conditional terms and the function being defined.  While we
use the case of two arguments as an example, our considerations apply also
to functions of different numbers of arguments and to collections
of mutually recursive programs.

	In order to evaluate a LISP function applied to given arguments
we first regard the program as an equation and substitute the arguments of
the function for the variables.  Thus to compute (A B)*(C D), we first
write

⊗⊗⊗(A B) * (C D) ← qif qn (A B) qthen (C D) qelse qa (A B) . [qd (A B) * (C D)]⊗.

The value of the expression on the left
is then obtained by evaluating the right hand
side.  This evaluation is accomplished according to
the following rules:

	1. We evaluate from left to right and from the inside out.  
Thus we evaluate the arguments of a function before evaluating the
expression.

	2. The conditional term ⊗⊗qif p qthen a qelse b⊗ is not regarded
as a function of ⊗p, ⊗a, and ⊗b.  To do so would involve evaluating all
three of ⊗p, ⊗a and ⊗b before evaluating the expression.  Instead
⊗⊗qif p qthen a qelse b⊗
is evaluated by first evaluating the condition ⊗p  and then evaluating  ⊗a 
or ⊗b (but not both) according to whether  ⊗p  is true or false.  If
the evaluation of  ⊗p  is unsuccessful then the conditional term
is considered to have no value.  Thus even  ⊗⊗qif p qthen qnil qelse qnil⊗ has
no value if ⊗p  has no value.

	3. Elementary LISP functions applied to S-expressions are
evaluated as described in chapter {section readin}.

	4. A recursively defined function applied to arguments is evaluated
after its arguments have been evaluated by again replacing the instance
of the left hand
side of its definition by the corresponding instance of its right hand side.


	Thus according to these rules we evaluate ⊗⊗(A)_*_(B_C)⊗ by
writing

(A) * (B C) ← if qn (A) qthen (B C) qelse qa (A) . [qd (A) * (B C)]

	← if false qthen (B C) qelse qa (A) . [qd (A) * (B C)]

	← qa (A) . [qd (A) * (B C)]

	← A . [qd (A) * (B C)]

	← A . [qnil * (B C)]

	← A . [qif qn qnil qthen (B C) qelse qa qnil . [qd qnil * (B C)]]

	← A . [qif true qthen (B C) qelse qa qnil . [qd qnil * (B C)]]

	← A . (B C)

	← (A B C)

Actual LISP systems use recursive subroutines rather than substitution,
but the value is the same as if computed in this way.
xxxxx
[PERHAPS THE ABOVE SHOULD BE A DISPLAYED FIGURE]

	The following example (adapted from one by
James Morris) shows an unexpected consequence
of the above rule.  We define

⊗⊗⊗morris[u,v] ← qif qn u qthen qnil qelse morris[qd u, morris[u,v]]⊗.

According to the above rules  ⊗⊗morris[(A),qnil]⊗
is to be evaluated as follows:

⊗⊗⊗morris[(A),qnil] ← qif qn (A) qthen qnil qelse morris[qd (A), morris[(A),qnil]]⊗

		← qif false qthen qnil qelse morris[qd (A), morris[(A),qnil]]

		← morris[qd (A), morris[(A),qnil]]

		← morris[qnil, morris[(A),qnil]]

At this point we are stuck, because according to our rules, we must evaluate
morris[(A),qnil]   before proceeding further with the main evaluation,
and this is the expression we started with.
Indeed all the main LISP systems
will go into a loop on this evaluation.  However, were we to
use the program as an equation to
expand the outer ⊗morris, the evaluation could continue as follows:

		← qif qn qnil qthen qnil else morris[qd qnil,morris[(A),qnil]]

		← qif true qthen qnil qelse morris[qd qnil,morris[(A),qnil]]

		← qnil

According our rules, these further
steps are not permitted.  In chapter {section comput} we shall mention alternate
(call-by-name or call-by-need) rules of
evaluation in which the answer qnil is obtained and discuss interpreters
that work accordingly.

	Converting the program into a sentence is subject to the following
rules.

	1. Quantification is over the domain of arguments of the
function.  In the above cases, this is the domain of lists.

	2. It %2may not be%1 assumed that the value of the function is in
the domain of arguments.  This must be proved when true.
In the case of ⊗append, we will be able to prove

⊗⊗⊗∀u v.islist[u*v]⊗,

expressing the fact that the computation of ⊗u*v always terminates and
gives a list as values.  However, we will be able to prove that
⊗morris(u,v) is a list only for  ⊗⊗u_=_qnil⊗.
Because of this, the three steps leading to the conclusion
⊗⊗morris[(A),qnil]_=_qnil⊗
won't be valid, since using (*) to subsitute for the outer ⊗morris 
would depend on knowing that  ⊗morris[(A),qnil]  was a list.
Thus the logic and the LISP computation nicely correspond.


new outline
1. introduction - skill rather than abstract knowledge.  Present
introduction is mainly ok.

2. Logic including first order λs, cond. exprs. and sorts.  Examples
to include some things needed later including perhaps bottom.

3. Theory of elementary LISP functions, car cdr cons
proof that ∀x.y.x ≠ x.  Perhaps a proof about subexp, e.g. ∀x.¬subexp(x,x).

4. Converting programs to sentences.

5. Proving extensional facts about programs.
append terminates
append is associative
flat[x,u] = flatten x * u

6. LISP "predicates".  samefringe

7. The Scott ordering or the minimization schema without it.

8. Proof checkers (appendix)

9. Exercises

1s(PROVIN,PROVING FACTS ABOUT LISP PROGRAMS)
2ss(formal,About Formalizing.)
3ss(sexpth, The theory of S-expressions.)
4ss(first, Summary of notion of formal theory.)
5ss(lispth, |Lists, natural numbers and LISP program primitives.|)
6ss(total,Representing programs known to terminate.)
7ss(partial,Representing programs not known to terminate.)
8ss(recpred,Recursively Defined Predicates.)
9ss(induction, Additional induction principles for proving.)
10s(minim,Partial functions and the Minimization Schema.)
11s(lispax,Theory of LISP: Algebraic Axioms.)
12s(provinex, Exercises )
logic for the Cobol programmer

THE LANGUAGE OF MATHEMATICAL LOGIC

LANGUAGES OF MATHEMATICAL LOGIC

	In order to prove facts about LISP programs, we
use languages of mathematical logic to express
the programs and the assertions we want to prove.
We can then use the rules of logic to prove
the assertions.  We present only as much of logic as is needed
for our purposes, but the student familiar with logic should skim
this section anyway, because it contains some extensions
convenient for expressing programs.  He should also note that
we confine ourselves to one intended interpretation and so avoid a
general discussion of interpretations and models.  Also we give no
proofs of metatheorems about logic although we give many proofs
of theorems about LISP functions within logic.

	We will be mainly interested in the domains of S-expressions,
lists and natural numbers, but other domains are important in
some problems.  We always consider our domains to be imbedded in
an unspecified outer domain.  This is because we will define functions
which are not a priori known to have S-expressions as values.
They have to be proved to yield S-expressions in particular cases.

	In order to define a logical language we must begin by defining the
expressions which can occur in it.  These definitions are mutually
inductive, since expressions of one kind can occur as sub-expressions
of others.  At the bottom we have constants and variables and then
we have terms, formulas, function expressions and predicate expresssions.
We begin with individual constants and individual variables.

1. Individual constants.  These include

	a. S-expressions.  These are written as described in Chapter I.
Examples include A, (A.B), (A B), (PLUS (TIMES X Y) 3), 3.73.
Thus numbers in any of the usual notations are included among S-expressions.

	b. Among the S-expressions, we distinguish natural numbers
and lists.  Examples of the natural numbers are 0, 1, 2 and 37, and
examples of of lists include (A B C) and (A (1 A) (2 B)).

2. Individual variables.  These range over various domains.  As in
previous chapters we use x, y and z with or without subscripts to range
over S-expressions, u, v and w for lists and m and n for natural numbers.
General variables, ranging over all objects, include X, Y and Z.
We call these individual variables to distinguish them from function
variables which we also need.

3. Function symbols.  These include function
constants such as ⊗car, ⊗cdr, ⊗cons and ⊗append and also function
variables like ⊗f, ⊗g and ⊗h. 
Each function symbol has an ⊗arity telling how many arguments it takes.
Further function symbols may be introduced by definitions.

4. Terms.  Terms are expressions whose values are numbers or S-expressions
or elements of other domains.
Variables and constants are terms and terms may be formed by
applying function expressions to previously formed terms.
Examples of terms are
⊗x, ⊗A, ⊗cons(x,A), ⊗cons(PLUS,_cons(X,cons(Y,NIL))).  When convenient
or customary infixes like + may be used to form terms.
Besides this, if ⊗p  is a sentence and  ⊗t1  and  ⊗t2  are terms, then

⊗⊗⊗IF p THEN t1 ELSE t2⊗

is a term.

Note to the logic student:  Conditional terms are not customary in
mathematical logic, but their use makes expressing facts about
recursive programs much more convenient.  They don't change the
metamathematics, because they can be eliminated at the
cost of making certain formulas longer.

5. Formulas.  Formulas are expressions that can be true or false depending
on the values of the constants, variables and functions that occur in them.
The truth-value of a formula is qtrue if
the formula is true and qfalse if it is false.
qtrue and qfalse are the two constant formulas.  We have propositional
variables ⊗p, ⊗q and ⊗r with or without subscripts.  If ⊗t1 and ⊗t2 are
terms, then ⊗⊗t1_=_t2⊗ is a formula.  If ⊗p is a predicate symbol of
(say) arity three and ⊗t1, ⊗t2 and ⊗t3 are terms, then ⊗p(t1,t2,t3) is
a formula whose truth depends in the obvious way on the predicate
represented by ⊗p and the values of ⊗t1, ⊗t2 and ⊗t3.  Formulas may
be combined by the propositional connectives ∧ (and), ∨ (or), ¬ (not),
⊃ (implies), ≡ (if and only if), and the ternary connective
(IF ... THEN ... ELSE ...).  The truth-value of a propositional combination of
formulas depends only on the truth-values of its constituents according
to the following ⊗⊗truth tables⊗.

xxxxx
****[Here go truth tables for the connectives including IF ... THEN ... ELSE]

	It is convenient to use the same notation for the conditional
terms used to combine formulas as is used for those that combine
a formula and two terms.

	New formulas can be obtained from old by ⊗quantification.  A
⊗quantifier is an expression of the form ⊗⊗∀x1 ... xn.⊗ or ⊗⊗∃x1 ... xn.⊗,
where the ⊗⊗x⊗s are variables.  Thus ⊗∀x, ⊗⊗∀x_y⊗ and ⊗⊗∃x_y_z⊗ are
quantifiers.  If ⊗Q is a quantifier and ⊗p is a formula, then
⊗Qp is a formula.  Here are some examples of formulas.

xxxxx
Expressions used in recursive programs

	The reader will have noted that the notation for the logical
connectives and conditional terms that we used in
the previous section on mathematical logic is different from that
used in chapters {section readin} and {section writin}.
This is because many of the "formulas" that we used in these chapters
cannot be regarded as formulas in logic but have to be treated as
terms.  There are two reasons.

	1. In existing LISP implementations the propositional operators
and conditional terms treat qnil as qfalse and every other
result as qtrue.  This makes possible expressions like

	⊗⊗qif x qthen f(x) qelse y⊗

where ⊗x is the result of some computation.  If this computation
gives any result but qnil, its result is regarded as true and can
be used in further computation as in the above example.  We can
use ⊗⊗x_or_y⊗ in a similar way.  If the value of ⊗x is anything
but qnil we get ⊗⊗x⊗.  Treating the LISP propositional connectives
simply as logical operators would give results that don't correspond
to the way LISP systems work.

	2. The second reason is deeper.  LISP computations don't
always terminate, and we want our theory to be able to treat
computations that are not assumed in advance to terminate.  Indeed
an important goal of our theory is to be able to prove that they
terminate.  As we shall see in the next section, not assuming
that they terminate amounts to allowing the possibility that the
value of a LISP expression is not an S-expression.  Among the
computations that may not terminate are those of propositional
expressions, and we msut allow for this possibility by admitting that
they sometimes take values other than qtrue or qfalse.

	This is handled by axiomatizing the LISP propositional
connectives in the following way:

⊗⊗⊗∀x y. issexp x ⊃ x and y = IF x = qnil THEN qnil ELSE y⊗.

Notice that this axiom says nothing about the value of ⊗⊗x_and_y⊗ when
⊗x is not an S-expression.  Notice also that ⊗⊗x_and_y⊗ is treated
as a term and not as a formula.  The other logical connectives are
axiomatized as similarly, namely:

⊗⊗⊗∀x y. issexp x ⊃ x or y = IF x = qnil THEN y ELSE x⊗.

⊗⊗⊗∀x. issexp x ⊃ not x = IF x = qnil THEN T ELSE qnil⊗.

⊗⊗⊗∀x y. issexp x ⊃ x implies y = IF x = qnil THEN T ELSE y⊗.

xxxxx for equiv

	LISP conditional terms are axiomatized by

⊗⊗⊗∀x y z.issexp x ⊃ qif x qthen y qelse z = IF x = qnil THEN z ELSE y⊗.

⊗⊗⊗∀x y z. issexp x ⊃ qif x qthen y qelse z = IF ¬NULL x THEN y ELSE z⊗.
Notes on the old chapter

1. The introductory section is ok.

2. Section 1 "about formalizing" is almost ok.  The word "understanding"
should be avoided, and the last paragraph is unclear, e.g. "it".

3. Section 2 "the elementary theory of car, cdr and cons" is unsatisfactory.
The set relations are not used in the formal theory except implicitly,
the separate domains for atoms and other S-expressions are confusing,
and the "formal proof" of EQPAIR is informal.
The student doesn't notice that the first appearance of ∀ is a definition.
The fact that phi is the name of the empty set isn't mentioned.

4. It is better to use a different name than to refer to an explanation
of NO-RPLACS.  Predicate parameters are used without it being clear whether
they are being defined.

{ ... } set notation is unexplained.
Proof techniques

	There needs to be a section on techniques for proving correctness.

#. Express the desired facts as a sentence.

#. Express the programs involved as sentences.

#. Decide what is to be proved inductively.  Sometimes
 it will be a generalization of the desired fact.

#. Identify the main induction determining the qF.  Sometimes the facts
can be proved without induction, but this is only true in easy cases.

#. Identify any lemmas that have to be proved inductively.

#. Determine what instantiations of basic facts, previous theorems,
definitions of functions and lemmas are required.

#. What replacements of equals for equals are needed?

#. What propositional calculus deductions and theory of equality deductions
are required?

	We also need a section or at least some remarks on what sets of
facts constitute a statement of correctness.

append is essentially characterized by its definition, because

nil * u = u

and

[x.u]*v = x.[u*v]

are both wanted and together determine the function.  Other functions
have more complicated desiderata.
The mathematicians' statements of existence and uniqueness play an
important and even formal role in advanced problems.